Nuprl Definition : ma-chooser
0,22
postcript
pdf
Chooser(
dec
)(
b
,
s
) == Case
dec
(
b
,
s
) of inl(
tr
)
inl(1of(2of(
tr
))) ; inr(
x
)
inr(
)
latex
Definitions
x
.
A
(
x
)
,
Case
b
of inl(
x
)
s
(
x
) ; inr(
y
)
t
(
y
)
,
f
(
a
)
,
inl(
x
)
,
1of(
t
)
,
2of(
t
)
,
inr(
x
)
,
FDL editor aliases
ma-chooser
origin
inl(1of(2of(tr))) ; inr(x) inr(
) inl(1of(2of(tr))) ; inr(x) inr() 
x.A(x) s(x) ; inr(y) t(y)